Nuprl Lemma : tree_subtype2
4,23
postcript
pdf
E
:Type. tree_con(
E
;Tree(
E
))
Tree(
E
)
latex
Definitions
S
T
,
tree_con(
E
;
T
)
,
t
T
,
Tree(
E
)
,
x
:
A
.
B
(
x
)
Lemmas
tree
wf
,
tree
con
wf
origin
E:Type. tree_con(E;Tree(E)) 
Tree(E) E:Type. tree_con(E;Tree(E)) Tree(E) T
Tx:A. B(x)